\section{C\'alculo Lambda}

\subsection{Sint\'axis}

\paragraph{T\'erminos}
$M ::= x \; | \; \mathsf{true} \;| \; \mathsf{false} \; | \; 0 \;             
            | \; \mathrm{if} \, M \, \mathrm{then} \, P \, 
                                    \mathrm{else} \, Q \; 
            | \; (\lambda x : \sigma . M) \; | \; MN$ \newline
$ \hspace*{3.95cm} | \; \mathsf{succ}(M) \; | \; \mathsf{pred}(M) \; 
            | \; \mathsf{iszero}(M) \;
            | \; \mathrm{let} \, x = M \, \mathrm{in} \, N $ 
            \newline 
$ \hspace*{3.95cm} | \; \{ \, l_i: M^{\; i = 1 \dots n}_i \, \} \; 
            | \; M.l \; | \; \mathsf{ref} \, M \; | \; !M \; 
            | \; M := N \; | \; l $
$            
| \; \mathsf{Unit} \;
| \; \mathrm{fix} \; M \;$
      
\vspace*{0.5cm}
%donde 
\begin{itemize}
    \item   $M, N, P$ y $Q$ son (sub)t\'erminos.
    \item   $\sigma$ es una expresi\'on de tipo.
    \item   $x \in \chi$ es un s\'imbolo de variable, y $\chi$ es un 
            conjunto infinito enumerable.
    \item   $\mathcal{L} = \{ \; l_1: \sigma_1 \; , \; 
                                l_2: \sigma_2\ \; , \; 
                                \dots \;, 
                                \; l_n: \sigma_n \; \}$ 
            un conjunto de etiquetas.
\end{itemize}
     
\vspace*{0.5cm}

\noindent
Construcci\'on alternativa para definir funciones recursivas:
$\mathsf{letrec} \, f : \sigma = \lambda x : \tau . \, M \, 
\mathrm{in} \, N$.\\
Puede escribirse en t\'erminos de fix:
$\mathsf{letrec} \, f = \mathsf{fix} \; (\lambda f : \sigma \rightarrow 
    \sigma. \lambda  : \tau . \, M) \, \mathrm{in} \, N$



\paragraph{Expresiones de Tipos}
$
\sigma ::= \mathsf{Bool} \; | \; \mathsf{Nat} \; 
            | \; \sigma \rightarrow \tau
            | \; \mathsf{unit} \; 
            | \; \{ \, l_i: \sigma^{\; i = 1 \dots n}_i \, \} \; 
            | \; \mathsf{Ref} \, \sigma \;
$

%Los t\'erminos pueden representarse como \'arboles sint\'acticos.

%\subsection{}
%
%\paragraph{Variables Libres} $ $
%
%\begin{table}[H]
%\begin{tabular}{r  c  l}
    %FV(x)       & =     & $\{x\}$\\
    %FV($\mathsf{true}$) = FV($\mathsf{false}$) = FV($0$)
            %& =     & $\emptyset$\\
    %FV($\mathrm{if} \, M \, \mathrm{then} \, P \, \mathrm{else} \, Q$)    
            %& =     &FV($M) \, \cup$ FV($P) \, \cup$ FV($Q$) \\
    %FV($\lambda x : \sigma . M$)    & =     &FV($M) \setminus \{x\}$ \\
    %FV($M N$)   & =     & FV($M) \, \cup$ FV($N$)
%\end{tabular}
%\end{table}  

\subsection{Sem\'antica}

\paragraph{Valores}
$
V ::= \mathsf{true} \;| \; \mathsf{false} \;        
        | \; \underline{n} \; 
        | \; \lambda x : \sigma . M        
        | \; \mathsf{unit} \; 
        | \; \{ \, l_i: V^{\; i = 1 \dots n}_i \, \} \; 
        | \; l \;
$

\vspace*{0.5cm}
\noindent
Nuevos juicios de evaluación   $| \, M \, | \, \mu \rightarrow M \, 
                                | \, \mu$

\vspace*{0.5cm}        
\noindent
$\mu [l \mapsto V]$ cambia el valor de $\mu (l)$ por $V$. \newline
$\mu \oplus [l \mapsto V]$ store extendido resultante de ampliar $\mu$ 
con una nueva asociaci\'on $l \mapsto V$. \newline
\indent
donde $\mu$ es un store (funci\'on parcial de direcciones de memoria 
a valores).


\paragraph{Forma Normal}
T\'ermino bien tipado que ya no puede ser reducido.

\paragraph{Sem\'antica Operacional} $ $ \newline
%Axiomas de evaluaci\'on: establecen que ciertos juicios de evaluaci\'on 
%son derivables.
%Reglas de evaluaci\'on: establecen que ciertos juicios de evaluaci\'on 
%son derivables siempre y cuando otros lo sean.

% Bool
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c}
    \textbf{E-IfTrue } &
    \framebox{$\displaystyle \, \frac{}
    {\mathrm{if} \, \mathsf{true} \, \mathrm{then} \, P \, 
    \mathrm{else} \, Q \rightarrow P}$} \\
    & \\
    \textbf{E-IfFalse } &
    \framebox{$\displaystyle \, \frac{}
    {\mathrm{if} \, \mathsf{false} \, \mathrm{then} \, P \, 
    \mathrm{else} \, Q \rightarrow Q}$} \\
    & \\
    \textbf{E-If } &
    \framebox{$\displaystyle \, \frac{M \rightarrow M'}
    {\mathrm{if} \, M \, \mathrm{then} \, P \, \mathrm{else} \, Q 
    \rightarrow \mathrm{if} \, M' \, \mathrm{then} \, P \, 
    \mathrm{else} \, Q}$} \\
    %& \\    
\end{tabular}
\end{table}    

% Aplicación
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c}
    \textbf{E-App1} &
    \framebox{$\displaystyle \, \frac{M_1 \rightarrow M'_1}
    {M_1 M_2 \rightarrow M'_1 M_2}$} \\
    & \\
    \textbf{E-App2} &
    \framebox{$\displaystyle \, \frac{M_2 \rightarrow M'_2}
    {V_1 M_2 \rightarrow V_1 M'_2}$} \\
    & \\
    \textbf{E-AppAbs} &
    \framebox{$\displaystyle \, \frac{}
    {(\lambda x : \sigma . M) V \rightarrow M\{x \leftarrow V\}}$} \\
    %& \\
\end{tabular}
\end{table}    

% Nat
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c}
    \textbf{E-Succ} &
    \framebox{$\displaystyle \, \frac{M \rightarrow M'}
    {\mathsf{succ}(M) \rightarrow \mathsf{succ}(M')}$} \\
    & \\
    \textbf{E-Pred} &
    \framebox{$\displaystyle \, \frac{M \rightarrow M'}
    {\mathsf{pred}(M) \rightarrow \mathsf{pred}(M')}$} \\
    & \\
    \textbf{E-PredZero} &
    \framebox{$\displaystyle \, \frac{}
    {\mathsf{pred}(0) \rightarrow 0}$} \\
    & \\
    \textbf{E-PredSucc} &
    \framebox{$\displaystyle \, \frac{}
    {\mathsf{pred(succ(} \underline{n} )) \rightarrow \underline{n}}$} \\
    & \\
    \textbf{E-IsZero} &
    \framebox{$\displaystyle \, \frac{M \rightarrow M'}
    {\mathsf{iszero}(M) \rightarrow \mathsf{iszero}(M')}$} \\
    & \\
    \textbf{E-IsZeroZero} &
    \framebox{$\displaystyle \, \frac{}
    {\mathsf{iszero}(0) \rightarrow \mathsf{true}}$} \\
    & \\
    \textbf{E-IsZeroSucc} &
    \framebox{$\displaystyle \, \frac{}
    {\mathsf{iszero(succ(} \underline{n} )) \rightarrow 
    \mathsf{false}}$} \\
    %& \\
\end{tabular}
\end{table}    

% Let
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c}   
    \textbf{E-Let} &
    \framebox{$\displaystyle \, \frac{M_1 \rightarrow M'_1}
    {\mathrm{let} \, x = M_1 \, \mathrm{in} \, M_2 \rightarrow 
    \mathrm{let} \, x = M_1' \, \mathrm{in} \, M_2}$} \\
    & \\
    \textbf{E-LetV} &
    \framebox{$\displaystyle \, \frac{}
    {\mathrm{let} \, x = V \, \mathrm{in} \, M \rightarrow 
    M\{x \leftarrow V\}}$} \\
    %& \\
\end{tabular}
\end{table}    

% Proyecciones y Records
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c}
    \textbf{E-ProjRcd} &
    \framebox{$\displaystyle \, 
    \frac{j = 1 \dots n}
    {\{ \, l_i: V^{\; i = 1 \dots n}_i \, \} . l_j 
    \rightarrow V_j}$} \\
    & \\
    \textbf{E-Proj} &
    \framebox{$\displaystyle \, \frac{M \rightarrow M'}
    {M.l \rightarrow M'.l}$} \\
    & \\
    \textbf{E-Rcd} &
    \framebox{\small{
    $\displaystyle \, \frac{M_j \rightarrow M'_j}
    {\{ \, l_i: V^{\; i = 1 \dots j-1}_i \, \}, l_j = M_j, 
    \{ \, l_i: V^{\; i = j + 1 \dots n}_i \, \} \rightarrow \newline
    \{ \, l_i: V^{\; i = 1 \dots j-1}_i \, \}, l_j = M'_j, 
    \{ \, l_i: V^{\; i = j + 1 \dots n}_i \, \} }$}} \\    
\end{tabular}
\end{table}

% Referencias
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c}
    \textbf{E-RefV} &
    \framebox{$\displaystyle \, \frac{l \notin \mathsf{Dom}\,(\mu)}
    {\mathsf{ref} \, V \; | \; \mu \rightarrow l \; | \; 
    \mu \oplus (l \mapsto V)}$} \\ 
    & \\
    \textbf{E-AppRef1} &
    \framebox{$\displaystyle \, 
    \frac{M_1 \; | \; \mu \rightarrow M'_1 \; | \; {\mu}'}
    {M_1 M_2 \; | \; \mu \rightarrow M'_1 M_2 \; | \; {\mu}'}$} \\
    & \\ 
    \textbf{E-AppRef2} &
    \framebox{$\displaystyle \, 
    \frac{M_2 \; | \; \mu \rightarrow M'_2 \; | \; {\mu}'}
    {V M_2 \; | \; \mu \rightarrow V M'_2 \; | \; {\mu}'}$} \\
    & \\ 
    \textbf{E-AppRefAbs} &
    \framebox{$\displaystyle \, 
    \frac{}
    {(\lambda x : \sigma . M) V \; | \; \mu \rightarrow M 
    \{x \leftarrow V\} \; | \; \mu}$} \\
    & \\ 
    \textbf{E-Deref} &
    \framebox{$\displaystyle \, 
    \frac{M_1 \; | \; \mu \rightarrow M'_1 \; | \; {\mu}'}
    {!M_1 \; | \; \mu \rightarrow !M'_1 \; | \; {\mu}'}$} \\
    & \\ 
    \textbf{E-DerefLoc} &
    \framebox{$\displaystyle \, 
    \frac{\mu(l) = V}
    {!l \; | \; \mu \rightarrow V \; | \; {\mu}}$} \\
    & \\ 
    \textbf{E-Assign1} &
    \framebox{$\displaystyle \, 
    \frac{M_1 \; | \; \mu \rightarrow M'_1 \; | \; {\mu}'}
    {M_1 := M_2 \; | \; \mu \rightarrow !M'_1 := M_2 \; 
    | \; {\mu}'}$} \\
    & \\ 
    \textbf{E-Assign2} &
    \framebox{$\displaystyle \, 
    \frac{M_2 \; | \; \mu \rightarrow M'_2 \; | \; {\mu}'}
    {V := M_2 \; | \; \mu \rightarrow V := M'_2 \; 
    | \; {\mu}'}$} \\
    & \\ 
    \textbf{E-Assign} &
    \framebox{$\displaystyle \, 
    \frac{}
    {l := V \; | \; \mu \rightarrow \mathsf{unit} \; 
    | \; \mu[l \mapsto V]}$} \\
    & \\ 
    \textbf{E-Ref} &
    \framebox{$\displaystyle \, 
    \frac{M \; | \; \mu \rightarrow M' \; | \; {\mu}'}
    {\mathsf{ref} \, M \; | \; \mu \rightarrow \mathsf{ref} \, M' \; 
    | \; {\mu}'}$} \\
    & \\ 
    \textbf{E-RefV} &
    \framebox{$\displaystyle \, 
    \frac{l \notin \mathsf{Dom} \, (\mu)}
    {\mathsf{ref} \, V \; | \; \mu \rightarrow l \; 
    | \; \mu \oplus (l \mapsto V)}$} \\
    & \\ 
\end{tabular}
\end{table}

% Fix
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c} 
    \textbf{E-Fix } &
    \framebox{$\displaystyle \, 
    \frac{M \rightarrow M^{'}}
    {\mathrm{fix} \; M \rightarrow \mathrm{fix} \; M^{'}}$} \\
    & \\
    \textbf{E-FixBeta } &
    \framebox{$\displaystyle \, \frac{}    
    {\mathrm{fix} \; (\lambda x : \sigma . M) \rightarrow M 
    \{ x \leftarrow \, \mathrm{fix} \; (\lambda x : \sigma . M) \} }$} \\
\end{tabular}
\end{table}   

\paragraph{Lemas}
%\paragraph{Propiedades y Lemas}

\begin{itemize}
    \item   \textbf{Determinismo del Juicio de Evaluaci\'on en 
                    un paso} \newline
            Si $M \rightarrow M'$ y $M \rightarrow M''$
            entonces $M' = M''$.
    \item   Todo valor est\'a en una forma normal.
\end{itemize}

\paragraph{Evaluaci\'on en Muchos Pasos}
$\twoheadrightarrow$ es la clausura reflexiva transitiva 
de $\rightarrow$.
Es decir es la menor relaci\'on tal que
\begin{itemize}
    \item   Si $M \rightarrow M'$, entonces $M \twoheadrightarrow M'$.
    \item   $M \twoheadrightarrow M$ para todo $M$.
    \item   Si $M \twoheadrightarrow M'$ y $M' \twoheadrightarrow M''$, 
            entonces $M \twoheadrightarrow M''$.
\end{itemize}

\paragraph{Lemas}

\begin{itemize}
    \item   \textbf{Unicidad de las Formas Normales} \newline
            Si $M \twoheadrightarrow U$ y $M \twoheadrightarrow V$, 
            donde $U$ y $V$ son formas normales, entonces $U = V$.
    \item   \textbf{Terminaci\'on} \newline
            Para todo $M$, existe una forma normal $N$ tal que 
            $M \twoheadrightarrow N$.
\end{itemize}


\subsection{Tipado}

\paragraph{Contexto de Tipado}
Conjunto de pares $<x_i: \sigma_i>.$ \newline
El contexto de tipado $\Gamma$ es de la forma $\{ \, x_1: \sigma_1 \, , 
\, x_2: \sigma_2\ \, , \, \dots \,, \, x_n: \sigma_n \, \}$ 

\paragraph{Juicio de Tipado}
Expresi\'on de la forma $\Gamma \rhd M : \sigma$. \newline
Significa que el t\'ermino $M$ tiene tipo $\sigma$ suponiendo 
un contexto $\Gamma$.

\paragraph{Axiomas de Tipado} $ $ \newline

% Variables y Aplicaciones
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c}
    \textbf{T-Var } &
    \framebox{$\displaystyle \, \frac{x:\sigma \in \Gamma}
    {\Gamma \rhd x : \sigma}$} \\
    & \\
    \textbf{T-App } &
    \framebox{$\displaystyle \, 
    \frac{\Gamma \rhd M : \sigma \rightarrow \tau 
    \hspace*{1cm} \Gamma \rhd N : \sigma}
    {\Gamma \rhd MN : \tau}$} \\
    %& \\
\end{tabular}
\end{table}    

% Bool
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c} 
    \textbf{T-True } &
    \framebox{$\displaystyle \, \frac{}
    {\Gamma \rhd \mathsf{true} : \mathsf{Bool}}$} \\
    & \\
    \textbf{T-False } &
    \framebox{$\displaystyle \, \frac{}
    {\Gamma \rhd \mathsf{false} : \mathsf{Bool}}$} \\
    & \\
    \textbf{T-If } &
    \framebox{$\displaystyle \, 
    \frac{\Gamma \rhd M : \mathsf{Bool}
    \hspace*{1cm} \Gamma \rhd P : \sigma
    \hspace*{1cm} \Gamma \rhd Q : \sigma}
    {\Gamma \rhd \mathrm{if} \, M \, \mathrm{then} \, P \, 
    \mathrm{else} \, Q : \sigma}$} \\
    %& \\
\end{tabular}
\end{table}    

% Abstracciones Lambda
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c} 
    \textbf{T-Abs } &
    \framebox{$\displaystyle \, 
    \frac{\Gamma, x : \tau \rhd M : \sigma}    
    {\Gamma \rhd \lambda x : \sigma . M: \sigma \rightarrow \tau}$} \\
    %& \\
\end{tabular}
\end{table}    

% Nat
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c} 
    \textbf{T-Zero } &
    \framebox{$\displaystyle \, \frac{}
    {\Gamma \rhd 0 : \mathsf{Nat}}$} \\
    & \\
    \textbf{T-Succ } &
    \framebox{$\displaystyle \, \frac{\Gamma \rhd M : \mathsf{Nat}}
    {\Gamma \rhd \mathsf{succ}(M) : \mathsf{Nat}}$} \\
    & \\
    \textbf{T-Pred } &
    \framebox{$\displaystyle \, \frac{\Gamma \rhd M : \mathsf{Nat}}
    {\Gamma \rhd \mathsf{pred}(M) : \mathsf{Nat}}$} \\
    & \\
    \textbf{T-IsZero } &
    \framebox{$\displaystyle \, \frac{\Gamma \rhd M : \mathsf{Nat}}
    {\Gamma \rhd \mathsf{iszero}(M) : \mathsf{Bool}}$} \\
    %& \\
\end{tabular}
\end{table}

% Let
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c} 
    \textbf{T-Let } &
    \framebox{$\displaystyle \, 
    \frac{\Gamma \rhd M : \sigma_1
    \hspace*{1cm} \Gamma, x : \sigma_1 \rhd N : \sigma_2}
    {\Gamma \rhd \mathrm{let} \, x = M \, \mathrm{in} \, N : 
        \sigma_2}$} \\
    %& \\
\end{tabular}
\end{table}    

% Unit
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c}
    \textbf{T-Unit } &
    \framebox{$\displaystyle \, \frac{}
    {\Gamma \rhd \mathsf{unit} : \mathsf{Unit}}$} \\
\end{tabular}
\end{table}  

% Records y Proyecciones
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c} 
    \textbf{T-Rcd } &
    \framebox{$\displaystyle \, 
    \frac{\Gamma \rhd M_i : \sigma_i
    \hspace*{0.3cm} \mathrm{para \, cada} \; i = 1 \dots n}
    {\Gamma \rhd  \{ \, l_i: M^{\; i = 1 \dots n}_i \, \} : 
    \{ \, l_i: \sigma^{\; i = 1 \dots n}_i \, \}}$} \\
    & \\
    \textbf{T-Proj } &
    \framebox{$\displaystyle \, 
    \frac{\Gamma \rhd M : \{ \, l_i: \sigma^{\; i = 1 \dots n}_i \, \}
    \hspace*{0.3cm} \; j = 1 \dots n}
    {\Gamma \rhd M.l_j : \sigma_j }$} \\
    & \\
\end{tabular}
\end{table}

% Referencias
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c} 
    \textbf{T-Ref } &
    \framebox{$\displaystyle \, 
    \frac{\Gamma | \Sigma \rhd M : \sigma}    
    {\Gamma | \Sigma \rhd \mathsf{ref} \, M : 
            \mathsf{Ref} \, \sigma}$} \\
    & \\
    \textbf{T-DeRef } &
    \framebox{$\displaystyle \, 
    \frac{\Gamma | \Sigma \rhd M : \mathsf{Ref} \, \sigma}  
    {\Gamma | \Sigma \rhd !M : \sigma}$} \\
    & \\
    \textbf{T-Assign } &
    \framebox{$\displaystyle \, 
    \frac{\Gamma | \Sigma \rhd M_1 : \mathsf{Ref} \, \sigma_1
    \hspace*{1cm} \Gamma | \Sigma \rhd M_2 : \mathsf{Ref} \, \sigma_1}  
    {\Gamma | \Sigma \rhd M_1 := M_2 : \mathsf{Unit}}$} \\
    & \\
    \textbf{T-Loc } &
    \framebox{$\displaystyle \, 
    \frac{\Sigma(l) = \sigma}
    {\Gamma | \Sigma \rhd l : \mathsf{Ref} \, \sigma}$} \\
    & \\
\end{tabular}
\end{table}

% Fix
\begin{table}[H]
\begin{tabular}{p{2.7cm} | c} 
    \textbf{T-Fix } &
    \framebox{$\displaystyle \, 
    \frac{\Gamma \rhd M : \sigma \rightarrow \sigma}    
    {\Gamma \rhd \mathrm{fix} \; M : \sigma}$} \\
\end{tabular}
\end{table}   

\paragraph{Sistema de Tipado}
Sistema formal de deducci\'on o derivaci\'on, que utiliza axiomas y 
reglas de tipado para caracterizar un subconjunto de t\'erminos 
llamados tipados.

\paragraph{Objetivo} Garantizar la ausencia de estados de error. 
Si un t\'ermino cerrado est\'a bien tipado (y termina), entonces
eval\'ua a un valor.
Se considera un estado de error aquel estado que no es un valor pero 
en el que la ejecuci\'on est\'a trabada.

\paragraph{Correcci\'on} Progreso + Preservaci\'on.

\begin{itemize}
    \item   \textbf{Progreso}\newline
            Si $M$ es cerrado y bien tipado entonces ocurre alguna de 
            las siguientes situaciones
            \begin{enumerate}
                \item   $M$ es un valor.
                \item   existe $\, M^{'} \,$ tal que 
                        $M \rightarrow M^{'}$.
            \end{enumerate}          
            Es decir, la evaluaci\'on no puede trabarse para t\'erminos 
            cerrados, bien tipados que no son valores.

    \item   \textbf{Preservaci\'on}\newline
            Si $\Gamma \rhd M : \sigma$ y $M \rightarrow N$, entonces 
            $\Gamma \rhd N : \sigma$. \newline
            Es decir, la evaluaci\'on preserva tipos.
\end{itemize}

\paragraph{Reformulaci\'on}
Cuando se usan referencias estas cosas dejan de valer, hay que 
reformularlas. 
Puede que la sem\'antica no respete los tipos supuestos por el 
sistema de tipos para las direcciones.
Deben tiparse los stores.
Nuevo juicio de tipado 
$\Gamma \, | \, \Sigma \rhd \mu$ sii
\begin{enumerate}
    \item   Dom($\Sigma$) = Dom($\mu$) y
    \item   $\Gamma \, | \, \Sigma \rhd \mu(l) : \Sigma(l)$ para todo 
            $l \in $ Dom($\mu$).
\end{enumerate}
$\Sigma$ puede crecer por alguna asignaci\'on.

\vspace*{0.5cm}

\noindent \textbf{Progreso}\newline
Si $M$ es cerrado y bien tipado entonces ocurre alguna de las 
siguientes situaciones
\begin{itemize}
    \item   $M$ es un valor.
    \item   para cualquier store $\mu$ tal que 
            $\emptyset \, | \, \Sigma \rhd \mu,$ existen $M^{'}$ y 
            $\mu^{'}$ tales que $M|\mu \rightarrow M^{'} | \mu^{'}$.
\end{itemize}

\vspace*{0.5cm}

\noindent \textbf{Preservaci\'on}\newline
Si se cumple que 
\begin{itemize}
    \item   $\Gamma \, | \, \Sigma \rhd M : \sigma$
    \item   $M \rightarrow N$
    \item   $\Gamma \, | \, \Sigma \rhd \mu$
\end{itemize}
entonces existe $\Sigma^{'}$, con $\Sigma \subseteq \Sigma^{'}$; 
tal que $\Gamma \, | \, \Sigma^{'} \rhd N : \sigma$.



\paragraph{Propiedades}

\begin{itemize}
    \item   \textbf{Unicidad de Tipos} \newline
            Si $\Gamma \rhd M : \sigma$ y 
            $\Gamma \rhd M : \tau$ son derivables, entonces 
            $\sigma = \tau$.
    \item   \textbf{Weakening y Strengthening} \newline
            Si $\Gamma \rhd M : \sigma$ es derivable y 
            $\Gamma \, \cap \, \Gamma^{'}$ contiene a todas las 
            variables libres de $M$, entonces 
            $\Gamma^{'} \rhd M : \sigma$.

    \item   \textbf{Sustituci\'on} \newline
            Si $\Gamma, x : \sigma \rhd M : \tau$ y 
            $\Gamma \rhd N$ son derivables, entonces 
            $\Gamma \rhd M\{x \leftarrow N\} : \tau$ es derivable.
\end{itemize}

